theory PeterEv imports Main Peterson PeterBeh ClangEv SemReach SemReach2
begin

fun lastev :: "(('pn,'n,'m,'l) gevent \<Rightarrow> bool) \<Rightarrow> ('pn,'n,'m,'l) gevent ~=> ('pn,'n,'m,'l) gevent"
where 
  "lastev A e = (if (\<exists> e1 . e1 \<preceq> e \<and> A e1) then Some (SOME a. a \<preceq> e \<and> A a \<and> (\<forall> a'. a' \<preceq> e \<and> A a' \<longrightarrow> a' \<preceq> a)) else None)"

lemma lem_lastev_val:
  assumes a1:"\<exists> e1 . e1 \<preceq> e \<and> A e1"
  shows "\<exists> a . (lastev A e) = Some a \<and> a \<preceq> e \<and> A a \<and> (\<forall> a'. a' \<preceq> e \<and> A a' \<longrightarrow> a' \<preceq> a)"
proof -
  obtain cond where c1:"cond = (\<lambda> n . (\<exists> a . ge_n a = n \<and> a \<preceq> e \<and> A a) )" by blast
  from this a1 have "\<exists> n . cond n" by blast
  moreover from c1 have "\<forall> n . cond n \<longrightarrow> (n \<le> ge_n e)" using less_eq_gevent_def by blast
  ultimately obtain n0 where c2:"cond n0 \<and> (\<forall> n' . (cond n' \<longrightarrow> n' \<le> n0))" using natmax_helper by blast
  from this c1 obtain a where c3:"ge_n a = n0 \<and> a \<preceq> e \<and> A a" by blast
  have c4:"\<forall> a'. a' \<preceq> e \<and> A a' \<longrightarrow> a' \<preceq> a"
  proof clarify
    fix a'
    assume "a' \<preceq> e" "A a'"
    from this c1 have "cond (ge_n a')" by blast
    from this c2 c3 have "ge_n a' \<le> ge_n a" by simp
    then show "a' \<preceq> a" using less_eq_gevent_def by blast
  qed
  obtain f where c5:"f = (\<lambda> a . a \<preceq> e \<and> A a \<and> (\<forall> a'. a' \<preceq> e \<and> A a' \<longrightarrow> a' \<preceq> a))" by blast
  from c3 c4 c5 have "\<exists> a. f a" by blast
  moreover from a1 c5 have "(lastev A e) = Some (SOME a. f a)" by simp
  ultimately have "\<exists> a . (lastev A e) = Some a \<and> f a" by (metis some_eq_ex)
  from this c5 show ?thesis by simp
qed

lemma lem_lastev_some:
  assumes a1:"lastev A e = Some a"
  shows "a \<preceq> e \<and> A a \<and> (\<forall> a'. a' \<preceq> e \<and> A a' \<longrightarrow> a' \<preceq> a)"
proof -
  from a1 have "\<exists> e1 . e1 \<preceq> e \<and> A e1" by (cases "\<exists> e1 . e1 \<preceq> e \<and> A e1", auto)
  then obtain ae where "(lastev A e) = Some ae \<and> ae \<preceq> e \<and> A ae \<and> (\<forall> a'. a' \<preceq> e \<and> A a' \<longrightarrow> a' \<preceq> ae)" using lem_lastev_val by blast
  from this a1 show ?thesis by auto
qed

(*--------------------------------------------------------------------------------------------------------------------------------------------*)

definition "wcsP \<equiv> [Weq InterQ (Eimm (BoolV False)), Weq Turn (Eimm (BoolV True))]"
definition "waitstmP \<equiv> (Cwait None wcsP (Cnone (Some lcs)))"
definition "wcsQ \<equiv> [Weq InterP (Eimm (BoolV False)), Weq Turn (Eimm (BoolV False))]"
definition "waitstmQ \<equiv> (Cwait None wcsQ (Cnone (Some lcs)))"

--"first statement in a sequence"
fun fseq where "fseq (Cseq _ s _) = fseq s" | "fseq s = s"

definition "wh_bdy s = (case s of (Cwhile _ _ s') \<Rightarrow> s')" --"body of Cwhile"

--"statment s does not write to a shared variable x"
fun nwdetect where "nwdetect x s = (\<not> wdetect x s)"
--"is a critical section"
fun csdetect where "csdetect s = (fseq s = (Cnone (Some lcs)))"
--"is not a critical section"
fun ncsdetect where "ncsdetect s = (\<not> csdetect s)"

lemma cs_regular: "csdetect s \<Longrightarrow> nwdetect x s" by (induct s, auto)

lemma nwdetect_seqcond: "seqcond (nwdetect x)" by (simp add: seqcond_def)
lemma ncsdetect_seqcond: "seqcond (ncsdetect)" by (simp add: seqcond_def)

--"if s2 is a critical section in P, s1 is the last (writeto InterP) in P, then s1 writes True to InterP"
lemma wint_value_P:
assumes a1: "stmcl (Cwhile None be (wh_bdy (proc_stm psrc))) s1"
  and a2: "wdetect InterP s1"
  and a3: "astmcl (nwdetect InterP) s1 s2"
  and a4: "csdetect s2"
  shows "vdetect s1 = (Some T)"
using a1 a2 a3 a4
apply(cases s1, auto)
apply(cases s2, auto)
apply(case_tac "stmt1")
apply(auto simp add: wh_bdy_def psrc_def)
done

lemma ex_wint_bef_cs_P: "astmcl (nwdetect InterP) (proc_stm psrc) s \<Longrightarrow> csdetect s \<Longrightarrow> False"
  by (cases s, auto simp add: psrc_def)

lemma ex_wtur_bef_cs_P: "astmcl (nwdetect Turn) (proc_stm psrc) s \<Longrightarrow> csdetect s \<Longrightarrow> False"
  apply(cases s, auto simp add: psrc_def)
  by (case_tac "stmt1", auto)

lemma wait_bef_cs_P:
  assumes a1:"stmcl (Cwhile None be (wh_bdy (proc_stm psrc))) s1"
  and a2: "astmcl (\<lambda> s. fseq s \<noteq> waitstmP) s1 s2" "csdetect s2"
  shows "nwdetect Turn s1"
using a1 a2
apply(cases s1, auto)
apply(auto simp add: waitstmP_def wh_bdy_def psrc_def)
apply(case_tac "stmt1", auto)
apply(cases s2, auto)
apply(case_tac "stmt1", auto)
apply(case_tac "stmt1a", auto simp add: wcsP_def)
apply(case_tac "stmt1a", auto)
apply(case_tac "stmt1a", auto)
done

lemma waitstmP_rdet: "fseq s = waitstmP \<Longrightarrow> (\<forall> x . rdetect x s \<longrightarrow> (x = InterQ \<or> x = Turn)) \<and> (rdetect InterQ s \<or> rdetect Turn s)"
  by (induct s, auto simp add: waitstmP_def wcsP_def)

(*
lemma wait_bef_cs_P: "stmcl (Cwhile None be (wh_bdy (proc_stm psrc))) s \<Longrightarrow> transition s q io s' q' \<Longrightarrow> csdetect s' \<Longrightarrow> fseq s = waitstmP"
apply(cases s', auto)
apply(cases "eval_bexpr q be", simp_all)
apply(case_tac "a", simp_all)
apply(case_tac "bool", simp_all)

apply(simp add: psrc_def wh_bdy_def waitstmP_def)
apply(cases s, simp_all)
apply(case_tac "stmt1", auto)
apply(cases "eval_bexpr q be", simp_all)
apply(case_tac "a", simp_all)
apply(case_tac "bool", simp_all)

apply(cases "eval_bexpr q be", simp_all)
apply(case_tac "a", simp_all)
apply(case_tac "bool", simp_all)
apply(simp add: psrc_def wh_bdy_def waitstmP_def)

apply(cases s, auto)
defer
apply(cases "eval_bexpr q be", simp_all)
apply(case_tac "a", simp_all)
apply(case_tac "bool", simp_all)
apply(simp add: psrc_def wh_bdy_def waitstmP_def)

apply(case_tac "option", auto)
apply(simp add: psrc_def wh_bdy_def waitstmP_def)
apply(case_tac "stmt1", auto)
apply(case_tac "stmt1a", simp_all)
apply(case_tac "option", auto)
apply(case_tac "option", auto)
apply(case_tac "stmt1a", simp_all)
apply(case_tac "option", auto)
apply(case_tac "stmt1a", simp_all)
done
*)

lemma nowint_aft_tur_P:
  assumes a0:"stmcl (Cwhile None be (wh_bdy (proc_stm psrc))) s1"
  and a1: "wdetect Turn s1" "stmcl s1 s2"
  and a2: "astmcl (nwdetect Turn) s2 s3" "csdetect s3"
  shows "nwdetect InterP s2"
using a0 a1 a2
apply(cases s1)
apply(cases s3)
apply(auto simp add: wh_bdy_def psrc_def)
apply(case_tac "stmt1", auto)
apply(case_tac "stmt1", auto)

apply(cases s3, auto simp add: anoncls_def)
apply(cases s2, auto)
apply(cases s2, simp_all)
apply(case_tac "stmt1", auto)
apply(case_tac "stmt1a", auto)
apply(case_tac "stmt1a", auto)
apply(case_tac "stmt1a", auto)
apply(case_tac "stmt1a", auto)

apply(cases s2, auto)
apply(case_tac "stmt1", auto)
apply(case_tac "stmt1", auto)
apply(cases s3, auto)
apply(case_tac "stmt1", auto)
apply(case_tac "stmt1", auto)
apply(cases s3, auto)
apply(case_tac "stmt1", auto)
apply(case_tac "stmt1", auto)
apply(case_tac s3, auto)
apply(case_tac "stmt1", auto)
apply(case_tac "stmt1a", auto)
apply(case_tac "stmt1a", auto)
done

(*lemma nowint_aft_tur_P:
  assumes a0:"stmcl (Cwhile None be (wh_bdy (proc_stm psrc))) s1"
  and a1: "wdetect Turn s1"
  and a2: "astmcl (ncsdetect) s1 s2"
  shows "nwdetect InterP s2"
using a0 a1 a2
apply(cases s1)
apply(cases s2)
apply(auto simp add: wh_bdy_def psrc_def)
apply(case_tac "stmt1", auto)
apply(case_tac "stmt1", auto)
apply(cases s2, auto simp add: anoncls_def)
apply(case_tac "stmt1", auto simp add: anoncls_def)
apply(cases s2, auto simp add: anoncls_def)
apply(case_tac "stmt1", auto simp add: anoncls_def)
done*)

lemma wint_value_Q:
assumes a1: "stmcl (Cwhile None be (wh_bdy (proc_stm qsrc))) s1"
  and a2: "wdetect InterQ s1"
  and a3: "astmcl (nwdetect InterQ) s1 s2"
  and a4: "csdetect s2"
  shows "vdetect s1 = (Some T)"
using a1 a2 a3 a4
apply(cases s1, auto)
apply(cases s2, auto)
apply(case_tac "stmt1")
apply(auto simp add: wh_bdy_def qsrc_def)
done

lemma nowint_aft_tur_Q:
  assumes a0:"stmcl (Cwhile None be (wh_bdy (proc_stm qsrc))) s1"
  and a1: "wdetect Turn s1" "stmcl s1 s2"
  and a2: "astmcl (nwdetect Turn) s2 s3" "csdetect s3"
  shows "nwdetect InterQ s2"
using a0 a1 a2
apply(cases s1)
apply(cases s3)
apply(auto simp add: wh_bdy_def qsrc_def)
apply(case_tac "stmt1", auto)
apply(case_tac "stmt1", auto)

apply(cases s3, auto simp add: anoncls_def)
apply(cases s2, auto)
apply(cases s2, simp_all)
apply(case_tac "stmt1", auto)
apply(case_tac "stmt1a", auto)
apply(case_tac "stmt1a", auto)
apply(case_tac "stmt1a", auto)
apply(case_tac "stmt1a", auto)

apply(cases s2, auto)
apply(case_tac "stmt1", auto)
apply(case_tac "stmt1", auto)
apply(cases s3, auto)
apply(case_tac "stmt1", auto)
apply(case_tac "stmt1", auto)
apply(cases s3, auto)
apply(case_tac "stmt1", auto)
apply(case_tac "stmt1", auto)
apply(case_tac s3, auto)
apply(case_tac "stmt1", auto)
apply(case_tac "stmt1a", auto)
apply(case_tac "stmt1a", auto)
done

(*lemma nowint_aft_tur_Q:
  assumes a0:"stmcl (Cwhile None be (wh_bdy (proc_stm qsrc))) s1"
  and a1: "wdetect Turn s1"
  and a2: "astmcl (ncsdetect) s1 s2"
  shows "nwdetect InterQ s2"
using a0 a1 a2
apply(cases s1)
apply(cases s2)
apply(auto simp add: wh_bdy_def qsrc_def)
apply(case_tac "stmt1", auto)
apply(case_tac "stmt1", auto)
apply(cases s2, auto simp add: anoncls_def)
apply(case_tac "stmt1", auto simp add: anoncls_def)
apply(cases s2, auto simp add: anoncls_def)
apply(case_tac "stmt1", auto simp add: anoncls_def)
done*)

lemma ex_wint_bef_cs_Q: "astmcl (nwdetect InterQ) (proc_stm qsrc) s \<Longrightarrow> csdetect s \<Longrightarrow> False"
  by (cases s, auto simp add: qsrc_def)

lemma ex_wtur_bef_cs_Q: "astmcl (nwdetect Turn) (proc_stm qsrc) s \<Longrightarrow> csdetect s \<Longrightarrow> False"
  apply(cases s, auto simp add: qsrc_def)
  by (case_tac "stmt1", auto)

lemma wait_bef_cs_Q:
  assumes a1:"stmcl (Cwhile None be (wh_bdy (proc_stm qsrc))) s1"
  and a2: "astmcl (\<lambda> s. fseq s \<noteq> waitstmQ) s1 s2" "csdetect s2"
  shows "nwdetect Turn s1"
using a1 a2
apply(cases s1, auto)
apply(auto simp add: waitstmQ_def wh_bdy_def qsrc_def)
apply(case_tac "stmt1", auto)
apply(cases s2, auto)
apply(case_tac "stmt1", auto)
apply(case_tac "stmt1a", auto simp add: wcsQ_def)
apply(case_tac "stmt1a", auto)
apply(case_tac "stmt1a", auto)
done

lemma waitstmQ_rdet: "fseq s = waitstmQ \<Longrightarrow> ((\<forall> x . rdetect x s \<longrightarrow> (x = InterP \<or> x = Turn)) \<and> (rdetect InterP s \<or> rdetect Turn s))"
  by (induct s, auto simp add: waitstmQ_def wcsQ_def)

(*
lemma wait_bef_cs_Q: "stmcl (Cwhile None be (wh_bdy (proc_stm qsrc))) s \<Longrightarrow> transition s q io s' q' \<Longrightarrow> csdetect s' \<Longrightarrow> fseq s = waitstmQ"
apply(cases s', auto)
apply(cases "eval_bexpr q be", simp_all)
apply(case_tac "a", simp_all)
apply(case_tac "bool", simp_all)

apply(simp add: qsrc_def wh_bdy_def waitstmQ_def)
apply(cases s, simp_all)
apply(case_tac "stmt1", auto)
apply(cases "eval_bexpr q be", simp_all)
apply(case_tac "a", simp_all)
apply(case_tac "bool", simp_all)

apply(cases "eval_bexpr q be", simp_all)
apply(case_tac "a", simp_all)
apply(case_tac "bool", simp_all)
apply(simp add: qsrc_def wh_bdy_def waitstmQ_def)

apply(cases s, auto)
defer
apply(cases "eval_bexpr q be", simp_all)
apply(case_tac "a", simp_all)
apply(case_tac "bool", simp_all)
apply(simp add: qsrc_def wh_bdy_def waitstmQ_def)

apply(case_tac "option", auto)
apply(simp add: qsrc_def wh_bdy_def waitstmQ_def)
apply(case_tac "stmt1", auto)
apply(case_tac "stmt1a", simp_all)
apply(case_tac "option", auto)
apply(case_tac "option", auto)
apply(case_tac "stmt1a", simp_all)
apply(case_tac "option", auto)
apply(case_tac "stmt1a", simp_all)
done
*)


(*--------------------------------------------------------------------------------------------------------------------------------------------*)

fun Pi :: "(procnames,'n,'m,'l) gevent \<Rightarrow> bool"
  where "Pi e = (ge_proc e = ProcP)"

fun Qi :: "(procnames,'n,'m,'l) gevent \<Rightarrow> bool"
  where "Qi e = (ge_proc e = ProcQ)"

fun csi::"('pn,'n,'m,lbs) gevent \<Rightarrow> bool"
where
  "csi e = csdetect (ev_stm e)"

fun w_interPi::"(procnames,'n,shnames,lbs) gtrace \<Rightarrow> (procnames,'n,shnames,lbs) gevent ~=> (procnames,'n,shnames,lbs) gevent"
where
  "w_interPi tr e = (lastev (\<lambda> e'. globev tr e' \<and> writeto_ge InterP e' \<and> Pi e') e)"

fun w_turnPi::"(procnames,'n,shnames,lbs) gtrace \<Rightarrow> (procnames,'n,shnames,lbs) gevent ~=> (procnames,'n,shnames,lbs) gevent"
where
  "w_turnPi tr e = (lastev (\<lambda> e' . globev tr e' \<and> writeto_ge Turn e' \<and> Pi e') e)"

fun srPi::"(procnames,'n,shnames,lbs) gtrace \<Rightarrow> (procnames,'n,shnames,lbs) gevent ~=> (procnames,'n,shnames,lbs) gevent"
where
  "srPi tr e = (lastev (\<lambda> r . globev tr r \<and> stmlab (fseq (ev_stm r)) = None \<and> (read_ge InterQ r \<and> ge_val r = Some F \<or> read_ge Turn r \<and> ge_val r = Some AP) \<and> Pi r) e)"

fun w_interQi::"(procnames,'n,shnames,lbs) gtrace \<Rightarrow> (procnames,'n,shnames,lbs) gevent ~=> (procnames,'n,shnames,lbs) gevent"
where
  "w_interQi tr e = (lastev (\<lambda> e'. globev tr e' \<and> writeto_ge InterQ e' \<and> Qi e') e)"

fun w_turnQi::"(procnames,'n,shnames,lbs) gtrace \<Rightarrow> (procnames,'n,shnames,lbs) gevent ~=> (procnames,'n,shnames,lbs) gevent"
where
  "w_turnQi tr e = (lastev (\<lambda> e' . globev tr e' \<and> writeto_ge Turn e' \<and> Qi e') e)"

fun srQi::"(procnames,'n,shnames,lbs) gtrace \<Rightarrow> (procnames,'n,shnames,lbs) gevent ~=> (procnames,'n,shnames,lbs) gevent"
where
  "srQi tr e = (lastev (\<lambda> r . globev tr r \<and> stmlab (fseq (ev_stm r)) = None \<and> (read_ge InterP r \<and> ge_val r = Some F \<or> read_ge Turn r \<and> ge_val r = Some AQ) \<and> Qi r) e)"

lemma Pi_stmcl:
  assumes a0:"prog_semantics petalg tr" "globev tr e"
  and a1:"Pi e"
  shows "stmcl (proc_stm psrc) (ev_stm e)"
proof -
  have "psrc \<in> set petalg" by (auto simp add: petalg_def)
  moreover have "proc_name psrc = ProcP" by normalization
  moreover from a1 have "ge_proc e = ProcP" by simp
  ultimately show "stmcl (proc_stm psrc) (ev_stm e)" using a0 lem_init_stmcl by metis
qed

lemma Qi_stmcl:
  assumes a0:"prog_semantics petalg tr" "globev tr e"
  and a1:"Qi e"
  shows "stmcl (proc_stm qsrc) (ev_stm e)"
proof -
  have "qsrc \<in> set petalg" by (auto simp add: petalg_def)
  moreover have "proc_name qsrc = ProcQ" by normalization
  moreover from a1 have "ge_proc e = ProcQ" by simp
  ultimately show "stmcl (proc_stm qsrc) (ev_stm e)" using a0 lem_init_stmcl by metis
qed

(*-----------------------------------------------------------------------------------------------------------*)

lemma lem_complpq: --"axiom"
  assumes a0:"prog_semantics petalg tr \<and> globev tr e"
  shows "Pi e \<or> Qi e"
by (cases "ge_proc e", auto)

lemma lem_linpq: --"axiom"
  "prog_semantics petalg tr \<and> globev tr e1 \<and> globev tr e2 \<Longrightarrow> (Pi e1 \<and> Pi e2) \<or> (Qi e1 \<and> Qi e2) \<Longrightarrow> e1 = e2 \<or> e1 \<prec> e2 \<or> e2 \<prec> e1"
by (simp add: prog_semantics_def, metis lem_lin)

(*
lemma
  assumes a0: "prog_semantics petalg tr"
  and a1:"globev tr c" "Pi c" "csi (c::(procnames,'n,shnames,lbs) gevent)"
  shows "False"
proof -
  from a0 have c0: "valid_gtrace tr" using prog_semantics_def by blast
  obtain nc where c1:"nc = ge_n c" by blast
  obtain p where c2:"p = ge_proc c" by blast
  from a1 this have c3:"p = ProcP" by simp
  obtain proc where c4:"(proc::(procnames,'n,shnames,lbs) proc) = psrc" by blast

  from c0 c1 a1 c3 have "exseq tr p nc = Some (es_of_ev c)" using ev_in_exseq by simp
  obtain stmc qc ioc bvc where d1:"es_of_ev c = (Estate stmc qc ioc bvc)"
    by (cases "es_of_ev c", auto simp del: es_of_ev.simps)
  then have d2:"stmc = pstep_curstm (ge_stp c)" by simp
  from this a1 have d3:"stmlab stmc = Some lcsP \<or> stmlab stmc = Some lcsQ" by auto
  
  (*initialization*)
  from c3 c4 have "proc \<in> set petalg \<and> proc_name proc = p" by (simp, normalization)
  from a0 a1 c2 this obtain io0 bv0 where o1:"exseq tr p 0 = (Some (Estate (proc_stm proc) empty io0 bv0))" using exseq_init by blast
  (* step *)
  from c0 have o2:"\<forall> i . etrans (exseq tr p i) (exseq tr p (Suc i))" using exseq_trans by metis
  have "\<forall> i . (case (exseq tr p i) of Some (Estate stm _ _ _) \<Rightarrow> stm_srP stm | _ \<Rightarrow> True)"

qed
*)

(*------------------------------------------------------------------------------------------------------------------------------------------------------*)

lemma lem_winterP: --"axiom"
  fixes tr c u
  assumes a0:"prog_semantics petalg tr \<and> globev tr c"
  assumes a1:"Pi c \<and> csi c \<and> w_interPi tr c = Some u"
  shows "globev tr u \<and> writeto_ge InterP u \<and> ge_val u = Some T"
proof -
  from a0 have c0:"valid_gtrace tr" using prog_semantics_def by blast
  obtain cond where c1:"cond = (\<lambda> e'. globev tr e' \<and> writeto_ge InterP e' \<and> Pi e')" by blast
  from a1 c1 have c2:"lastev cond c = Some u" by simp
  then have "cond u" using lem_lastev_some by blast
  from this c1 have c3:"globev tr u \<and> writeto_ge InterP u \<and> Pi u" by simp
  moreover have "ge_val u = Some T"
  proof -
    from c3 a0 have "stmcl (proc_stm psrc) (ev_stm u)" using Pi_stmcl by blast
    moreover have "astmcl (nwdetect InterP) (ev_stm u) (ev_stm c)"
    proof -
      from c2 have d0:"u \<preceq> c"  using lem_lastev_some by blast
      from a1 c3 obtain p where d1:"p = ge_proc u \<and> p = ge_proc c" by simp
      have d2:"\<And> e . e \<in> {u<..c} \<and> globev tr e \<and> ge_proc e = p \<longrightarrow> nwdetect InterP (ev_stm e)"
      proof
        fix e
        assume z0:"e \<in> {u<..c} \<and> globev tr e \<and> ge_proc e = p"
        from z0 d1 c3 have z1:"Pi e" by simp
        {
          assume "wdetect InterP (ev_stm e)"
          from this z0 c0 have "writeto_ge InterP e" using lem_wdet by metis
          from this z0 c1 z1 have "cond e" by simp
          from z0 c2 this have "e \<preceq> u" using lem_lastev_some by auto
          moreover from z0 have "u \<prec> e" by auto
          ultimately have "False" by (metis less_le_not_le)
        }
        then show "nwdetect InterP (ev_stm e)" by auto
      qed
      from a1 have d3:"nwdetect InterP (ev_stm c)" using cs_regular by (metis csi.simps)
      from a0 c3 have "globev tr u \<and> globev tr c" by simp
      from c0 this d0 d1 d2 d3 show ?thesis using lem_ev_astmcl nwdetect_seqcond by metis
    qed
    moreover from c3 c0 have "wdetect InterP (ev_stm u)" using lem_wdet by metis
    ultimately have "vdetect (ev_stm u) = Some T" using a0 a1 wint_value_P
      by (auto simp add: psrc_def wh_bdy_def waitstmP_def)
    from c3 c0 this show ?thesis using lem_vdet by blast
  qed
  ultimately show ?thesis by blast
qed

lemma lem_lastwintP: --"axiom"
  fixes tr c u
  assumes a0:"prog_semantics petalg tr \<and> globev tr c"
  assumes a1:"Pi c \<and> csi c \<and> w_interPi tr c = Some u"
  shows "\<forall> e. globev tr e \<and> Pi e \<and> e \<in> {u..c} \<and> writeto_ge InterP e \<longrightarrow> e = u"
proof clarify
  fix e
  assume c0:"globev tr e" "Pi e" "e \<in> {u..c}" "writeto_ge InterP e"
  obtain cond where c1:"cond = (\<lambda> e'. globev tr e' \<and> writeto_ge InterP e' \<and> Pi e')" by blast
  from a1 c1 have "lastev cond c = Some u" by simp
  then have c2:"cond u \<and> (\<forall> a'. a' \<preceq> c \<and> cond a' \<longrightarrow> a' \<preceq> u)" using lem_lastev_some by blast
  from c0 c1 c2 have d1:"e \<preceq> u \<and> u \<preceq> e" by auto
  from c2 c1 c0 have d2:"globev tr e \<and> globev tr u" by auto
  from c2 c1 c0 have d3:"\<exists> p . is_proc_ev p u \<and> is_proc_ev p e" by auto
  from a0 d2 d3 have "e = u \<or> e \<prec> u \<or> u \<prec> e" using langevents.axlin by blast
  from this d1 show "e = u" by (metis less_le_not_le)
qed

lemma lem_wintQP: --"axiom"
  fixes tr e
  assumes a0:"prog_semantics petalg tr \<and> globev tr e"
  assumes a1:"writeto_ge InterQ e \<and> Pi e"
  shows "False"
proof -
  from a0 a1 have "stmcl (proc_stm psrc) (ev_stm e)" using Pi_stmcl by metis
  moreover from a1 have "wdetect InterQ (ev_stm e)" using lem_wdet a0 prog_semantics_def by metis
  moreover have "\<forall> s. stmcl (proc_stm psrc) s \<and> wdetect InterQ s \<longrightarrow> False"
    apply(auto)
    apply(case_tac s, simp_all)
    apply(case_tac "stmt1", auto)
    by (auto simp add: psrc_def)
  ultimately show ?thesis by blast
qed

lemma lem_wturnP_helper:
  fixes tr e
  assumes a0:"prog_semantics petalg tr \<and> globev tr e"
  assumes a1:"writeto_ge Turn e \<and> Pi e"
  shows "ge_val e = Some AQ"
proof -
  from a0 a1 have "stmcl (proc_stm psrc) (ev_stm e)" using Pi_stmcl by metis
  moreover from a1 have "wdetect Turn (ev_stm e)" using lem_wdet a0 prog_semantics_def by metis
  moreover have "\<And> s. stmcl (proc_stm psrc) s \<and> wdetect Turn s \<longrightarrow> vdetect s = Some AQ"
    apply(case_tac s)
    apply(auto simp add: psrc_def)
    by (case_tac "stmt1", auto)
  ultimately have "vdetect (ev_stm e) = Some AQ" by blast
  from this a0 show "ge_val e = Some AQ" using lem_vdet prog_semantics_def by blast
qed

lemma lem_wturnP: --"axiom"
  fixes tr c w
  assumes a0:"prog_semantics petalg tr \<and> globev tr c"
  assumes a1:"Pi c \<and> csi c \<and> w_turnPi tr c = Some u"
  shows "globev tr u \<and> writeto_ge Turn u \<and> ge_val u = Some AQ"
proof -
  obtain cond where c1:"cond = (\<lambda> e'. globev tr e' \<and> writeto_ge Turn e' \<and> Pi e')" by blast
  from a1 c1 have "lastev cond c = Some u" by simp
  then have "cond u" using lem_lastev_some by blast
  from this c1 have c2:"globev tr u \<and> writeto_ge Turn u \<and> Pi u" by simp
  from a0 this have "ge_val u = Some AQ" using lem_wturnP_helper by blast
  from this c2 show ?thesis by blast
qed

lemma lem_lastwturP: --"axiom"
  fixes tr c w
  assumes a0:"prog_semantics petalg tr \<and> globev tr c"
  assumes a1:"Pi c \<and> csi c \<and> w_turnPi tr c = Some w"
  shows "\<forall>a. globev tr a \<and> Pi a \<and> a \<in> {w..c} \<and> writeto_ge Turn a \<longrightarrow> a = w"
proof clarify
  fix e
  assume c0:"globev tr e" "Pi e" "e \<in> {w..c}" "writeto_ge Turn e"
  obtain cond where c1:"cond = (\<lambda> e'. globev tr e' \<and> writeto_ge Turn e' \<and> Pi e')" by blast
  from a1 c1 have "lastev cond c = Some w" by simp
  then have c2:"cond w \<and> (\<forall> a'. a' \<preceq> c \<and> cond a' \<longrightarrow> a' \<preceq> w)" using lem_lastev_some by blast
  from c0 c1 c2 have d1:"e \<preceq> w \<and> w \<preceq> e" by auto
  from c2 c1 c0 have d2:"globev tr e \<and> globev tr w" by auto
  from c2 c1 c0 have d3:"\<exists> p . is_proc_ev p w \<and> is_proc_ev p e" by auto
  from a0 d2 d3 have "e = w \<or> e \<prec> w \<or> w \<prec> e" using langevents.axlin by blast
  from this d1 show "e = w" by (metis less_le_not_le)
qed

lemma lem_wturnrP: --"axiom"
  fixes tr e
  assumes a0:"prog_semantics petalg tr \<and> globev tr e"
  assumes a1:"writeto_ge Turn e \<and> ge_val e = Some AP \<and> Pi e"
  shows "False"
using a0 a1
apply(subgoal_tac "ge_val e = Some AQ")
apply(clarsimp)
apply(metis lem_wturnP_helper)
done

lemma lem_srP: --"axiom"
  fixes tr c r
  assumes a0:"prog_semantics petalg tr \<and> globev tr c"
  assumes a1:"Pi c \<and> csi c \<and> srPi tr c = Some r"
  shows "globev tr r \<and> (read_ge InterQ r \<and> ge_val r = Some F \<or> read_ge Turn r \<and> ge_val r = Some AP)"
proof -
  obtain cond where c1:"cond = (\<lambda> r . globev tr r \<and> stmlab (fseq (ev_stm r)) = None \<and> (read_ge InterQ r \<and> ge_val r = Some F \<or> read_ge Turn r \<and> ge_val r = Some AP) \<and> Pi r)" by blast
  from a1 c1 have "lastev cond c = Some r" by simp
  then have "cond r" using lem_lastev_some by blast
  from this c1 show ?thesis by blast
qed

lemma lem_cordP: --"axiom"
  fixes tr
  and c::"((procnames, 'n, shnames, lbs) gevent)"
  assumes a0:"prog_semantics petalg tr \<and> globev tr c"
  assumes a1:"Pi c \<and> csi c"
  shows "\<exists> u w r. globev tr u \<and> globev tr w \<and> globev tr r \<and> Pi u \<and> Pi w \<and> Pi r \<and> w_interPi tr c = Some u \<and> w_turnPi tr c = Some w \<and> srPi tr c = Some r \<and> u \<prec> w \<and> w \<prec> r \<and> r \<prec> c"
proof -
  from a0 have c0:"valid_gtrace tr" using prog_semantics_def by blast
  obtain A_int where c1:"A_int = (\<lambda> e'. globev tr e' \<and> writeto_ge InterP e' \<and> Pi e')" by blast
  obtain A_turn where c2:"A_turn = (\<lambda> e' . globev tr e' \<and> writeto_ge Turn e' \<and> Pi e')" by blast
  obtain A_sr where c3:"A_sr = (\<lambda> r . globev tr r \<and> stmlab (fseq (ev_stm r)) = None \<and> (read_ge InterQ r \<and> ge_val r = Some F \<or> read_ge Turn r \<and> ge_val r = Some AP) \<and> Pi r)" by blast

  have "\<exists> u1 . u1 \<preceq> c \<and> A_int u1"
  proof -
    { assume "\<forall> e' \<le> c . globev tr e' \<and> ge_proc e' = ProcP \<longrightarrow> nwdetect InterP (ev_stm e')"
      moreover from a1 have "ProcP = proc_name psrc \<and> ProcP = ge_proc c" by (simp only: Pi.simps, normalization)
      moreover have "psrc \<in> set petalg" by normalization
      ultimately have "astmcl (nwdetect InterP) (proc_stm psrc) (ev_stm c)" using a0 nwdetect_seqcond lem_init_astmcl by metis
      from this a1 have "False" using ex_wint_bef_cs_P by (simp only: csi.simps, blast)
    }
    then obtain u1 where "u1 \<preceq> c \<and> globev tr u1 \<and> Pi u1 \<and> wdetect InterP (ev_stm u1)" by (metis Pi.simps nwdetect.simps)
    moreover then have "writeto_ge InterP u1" using c0 lem_wdet by metis
    ultimately show ?thesis using c1 by auto
  qed
  from this c1 obtain u where d1:"w_interPi tr c = Some u" using lem_lastev_val by auto
  from this c1 have d1':"A_int u \<and> u \<preceq> c" using lem_lastev_some by (auto simp only: w_interPi.simps)
  from this c1 have d1'':"globev tr u \<and> Pi u" by simp

  have "\<exists> w1 . w1 \<preceq> c \<and> A_turn w1"
  proof -
    { assume "\<forall> e' \<le> c . globev tr e' \<and> ge_proc e' = ProcP \<longrightarrow> nwdetect Turn (ev_stm e')"
      moreover from a1 have "ProcP = proc_name psrc \<and> ProcP = ge_proc c" by (simp only: Pi.simps, normalization)
      moreover have "psrc \<in> set petalg" by normalization
      ultimately have "astmcl (nwdetect Turn) (proc_stm psrc) (ev_stm c)" using a0 nwdetect_seqcond lem_init_astmcl by metis
      from this a1 have "False" using ex_wtur_bef_cs_P by (simp only: csi.simps, blast)
    }
    then obtain u1 where "u1 \<preceq> c \<and> globev tr u1 \<and> Pi u1 \<and> wdetect Turn (ev_stm u1)" by (metis Pi.simps nwdetect.simps)
    moreover then have "writeto_ge Turn u1" using c0 lem_wdet by metis
    ultimately show ?thesis using c2 by auto
  qed
  from this c2 obtain w where d2:"w_turnPi tr c = Some w" using lem_lastev_val by auto
  from this c2 have d2':"A_turn w \<and> w \<preceq> c" using lem_lastev_some by (auto simp only: w_turnPi.simps)
  from this c2 have d2'':"globev tr w \<and> Pi w" by simp

  have er1: "\<exists> r1 . r1 \<preceq> c \<and> A_sr r1 \<and> w \<prec> r1"
  proof -
    {
      assume "astmcl (\<lambda> s. fseq s \<noteq> waitstmP) (ev_stm w) (ev_stm c)"
      moreover from a0 d2'' have "stmcl (proc_stm psrc) (ev_stm w)" using Pi_stmcl by blast
      moreover from a1 have "csdetect (ev_stm c)" by simp
      ultimately have "nwdetect Turn (ev_stm w)" using wait_bef_cs_P by (auto simp add: psrc_def wh_bdy_def waitstmP_def)
      moreover from d2' c2 have "writeto_ge Turn w" by simp
      ultimately have "False" using c0 d2'' by (auto simp only: lem_wdet nwdetect.simps)
    }
    moreover from a0 d2' d2'' a1 have "w \<preceq> c \<and> ge_proc w = ProcP \<and> ge_proc c = ProcP" by simp
    moreover from a1 have "(\<lambda> s . fseq s \<noteq> waitstmP) (ev_stm c)" by (simp add: waitstmP_def)
    moreover have "seqcond (\<lambda> s. fseq s \<noteq> waitstmP)" by (auto simp add: seqcond_def)
    ultimately obtain r1 where z1:"r1 \<in> {w<..c} \<and> globev tr r1 \<and> ge_proc r1 = ProcP \<and> \<not> (\<lambda> s . fseq s \<noteq> waitstmP) (ev_stm r1)" using c0 a0 d2'' lem_ev_astmcl [of "\<lambda> s . fseq s \<noteq> waitstmP" tr w c ProcP] by metis
    then have z2:"r1 \<preceq> c \<and> globev tr r1 \<and> Pi r1" by simp
    moreover have "read_ge InterQ r1 \<and> ge_val r1 = Some F \<or> read_ge Turn r1 \<and> ge_val r1 = Some AP"
    proof -
      from z1 have g0:"fseq (ev_stm r1) = waitstmP" by simp
      then have "read_ge InterQ r1 \<or> read_ge Turn r1" using waitstmP_rdet c0 z2 lem_rdet by metis
      moreover have "read_ge InterQ r1 \<longrightarrow> ge_val r1 = Some F"
      proof
        assume "read_ge InterQ r1"
        moreover then obtain a where g1:"ge_val r1 = Some a" using read_ge_val by metis
        ultimately have h1:"\<And> wcs . wcsdetect (ev_stm r1) = Some wcs \<Longrightarrow> r_compat_wcs InterQ a wcs" using lem_wcsdet [of tr r1 InterQ a] using c0 z2 by blast
        moreover have "wcsdetect (ev_stm r1) = Some wcsP"
        proof -
          have "\<And> s . fseq s = waitstmP \<longrightarrow> wcsdetect s = Some wcsP" by (induct_tac s, auto simp add: waitstmP_def)
          from this g0 show ?thesis by blast
        qed
        ultimately have "r_compat_wcs InterQ a (wcsP::('n,shnames) wconds)" by metis
        then have "a = F" by (simp add: r_compat_wcs_def wcsP_def)
        from this g1 show "ge_val r1 = Some F"  by simp
      qed
      moreover have "read_ge Turn r1 \<longrightarrow> ge_val r1 = Some AP"
      proof
        assume "read_ge Turn r1"
        moreover then obtain a where g1:"ge_val r1 = Some a" using read_ge_val by metis
        ultimately have h1:"\<And> wcs . wcsdetect (ev_stm r1) = Some wcs \<Longrightarrow> r_compat_wcs Turn a wcs" using lem_wcsdet [of tr r1 Turn a] using c0 z2 by blast
        moreover have "wcsdetect (ev_stm r1) = Some wcsP"
        proof -
          have "\<And> s . fseq s = waitstmP \<longrightarrow> wcsdetect s = Some wcsP" by (induct_tac s, auto simp add: waitstmP_def)
          from this g0 show ?thesis by blast
        qed
        ultimately have "r_compat_wcs Turn a (wcsP::('n,shnames) wconds)" by metis
        then have "a = AP" by (simp add: r_compat_wcs_def wcsP_def)
        from this g1 show "ge_val r1 = Some AP"  by simp
      qed
      ultimately show ?thesis by blast
    qed
    moreover from z1 have "stmlab (fseq (ev_stm r1)) = None" by (simp add: waitstmP_def)
    ultimately have "r1 \<preceq> c \<and> A_sr r1" using c3 by simp
    from this z1 show ?thesis by auto
  qed
  then have "\<exists> r1 . r1 \<preceq> c \<and> A_sr r1" by blast
  from this c3 obtain r where d3:"srPi tr c = Some r" using lem_lastev_val by auto
  from this c3 have d3':"A_sr r \<and> r \<preceq> c" using lem_lastev_some by (auto simp only: srPi.simps)
  from this c3 have d3'':"globev tr r \<and> Pi r" by simp

  have f0:"\<And> e1 e2 . Pi e1 \<and> globev tr e1 \<and> Pi e2 \<and> globev tr e2 \<and> (e2 \<preceq> e1 \<longrightarrow> False) \<longrightarrow> e1 \<prec> e2"
  proof
    fix e1 e2
    assume z0:"Pi e1 \<and> globev tr e1 \<and> Pi e2 \<and> globev tr e2 \<and> (e2 \<preceq> e1 \<longrightarrow> False)"
    then have "ge_proc e1 = ge_proc e2 \<and> globev tr e1 \<and> globev tr e2" by simp
    from this c0 have "e1 = e2 \<or> e1 \<prec> e2 \<or> e2 \<prec> e1" using lem_lin by blast
    from this z0 show "e1 \<prec> e2" by (metis order_less_imp_le order_refl)
  qed

  have f1:"w \<preceq> u \<longrightarrow> False"
  proof
    assume z1:"w \<preceq> u"
    from a0 d2'' have "stmcl (proc_stm psrc) (ev_stm w)" using Pi_stmcl by blast
    moreover from c0 c2 d2' have "wdetect Turn (ev_stm w)" using lem_wdet by metis
    moreover from c0 d1'' d2'' z1 have "stmcl (ev_stm w) (ev_stm u)"
      by (subgoal_tac "ge_proc u = ProcP \<and> ge_proc w = ProcP", metis lem_ev_stmcl, auto)
    moreover have "astmcl (nwdetect Turn) (ev_stm u) (ev_stm c)"
    proof -
      have "\<forall> e \<in> {u<..c} . globev tr e \<and> ge_proc e = ProcP \<longrightarrow> nwdetect Turn (ev_stm e)"
      proof clarify
        fix e
        assume y1:"e \<in> {u<..c}" "globev tr e" "ge_proc e = ProcP"
        {
          assume "wdetect Turn (ev_stm e)"
          from this y1 c0 have "writeto_ge Turn e" using lem_wdet by metis
          from this c2 y1 have "e \<preceq> c \<and> A_turn e" by simp
          from this y1 d2 c2 have "e \<preceq> w" using lem_lastev_some [of "A_turn" c w] by auto
          moreover from y1 z1 have "w \<prec> e" by (auto simp add: order_le_less_trans)
          ultimately have "False" by (metis less_le_not_le)
        }
        then show "nwdetect Turn (ev_stm e)" by auto
      qed
      moreover from a1 have "nwdetect Turn (ev_stm c)" by (simp only: csi.simps cs_regular)
      moreover from d1'' a1 a0 have "ge_proc u = ProcP \<and> ge_proc c = ProcP" by simp
      ultimately show ?thesis using d1' d1'' a0 a1 c0 nwdetect_seqcond lem_ev_astmcl [of "nwdetect Turn" tr u c ProcP] by metis
    qed
    moreover from a1 have "csdetect (ev_stm c)" by simp
    ultimately have "\<not> wdetect InterP (ev_stm u)" using nowint_aft_tur_P by (auto simp add: psrc_def wh_bdy_def waitstmP_def)
    from this c0 c1 d1' show "False" using lem_wdet by metis
  qed
  from this d1'' d2'' have or1:"u \<prec> w" using f0 by blast

  have or2:"r \<prec> c"
  proof-
    from d3'' a1 have "ge_proc r = ge_proc c" by simp
    from d3'' a1 a0 this have "r = c \<or> r \<prec> c \<or> c \<prec> r" using lem_lin c0 by blast
    moreover from a1 c3 d3' have "r \<noteq> c" by auto (* use labels Some lcs and None *)
    ultimately show ?thesis using d3' by (metis less_le_not_le)
  qed

  have or3:"w \<prec> r"
  proof -
    from er1 obtain r1 where z1:"r1 \<preceq> c \<and> A_sr r1 \<and> w \<prec> r1" by blast
    moreover have "r1 \<preceq> r"
    proof -
      from d3 c3 have "lastev A_sr c = Some r" by simp
      from this z1 show ?thesis using lem_lastev_some [of A_sr c r] by blast
    qed
    ultimately show ?thesis using or2 by (metis order_less_le_trans)
  qed

  from d1 d1'' d2 d2'' d3 d3'' or1 or2 or3 show ?thesis by blast
qed

(*------------------------------------------------------------------------------------------------------------------------------------------------------*)

lemma lem_winterQ: --"axiom"
  fixes tr c u
  assumes a0:"prog_semantics petalg tr \<and> globev tr c"
  assumes a1:"Qi c \<and> csi c \<and> w_interQi tr c = Some u"
  shows "globev tr u \<and> writeto_ge InterQ u \<and> ge_val u = Some T"
proof -
  from a0 have c0:"valid_gtrace tr" using prog_semantics_def by blast
  obtain cond where c1:"cond = (\<lambda> e'. globev tr e' \<and> writeto_ge InterQ e' \<and> Qi e')" by blast
  from a1 c1 have c2:"lastev cond c = Some u" by simp
  then have "cond u" using lem_lastev_some by blast
  from this c1 have c3:"globev tr u \<and> writeto_ge InterQ u \<and> Qi u" by simp
  moreover have "ge_val u = Some T"
  proof -
    from c3 a0 have "stmcl (proc_stm qsrc) (ev_stm u)" using Qi_stmcl by blast
    moreover have "astmcl (nwdetect InterQ) (ev_stm u) (ev_stm c)"
    proof -
      from c2 have d0:"u \<preceq> c"  using lem_lastev_some by blast
      from a1 c3 obtain p where d1:"p = ge_proc u \<and> p = ge_proc c" by simp
      have d2:"\<And> e . e \<in> {u<..c} \<and> globev tr e \<and> ge_proc e = p \<longrightarrow> nwdetect InterQ (ev_stm e)"
      proof
        fix e
        assume z0:"e \<in> {u<..c} \<and> globev tr e \<and> ge_proc e = p"
        from z0 d1 c3 have z1:"Qi e" by simp
        {
          assume "wdetect InterQ (ev_stm e)"
          from this z0 c0 have "writeto_ge InterQ e" using lem_wdet by metis
          from this z0 c1 z1 have "cond e" by simp
          from z0 c2 this have "e \<preceq> u" using lem_lastev_some by auto
          moreover from z0 have "u \<prec> e" by auto
          ultimately have "False" by (metis less_le_not_le)
        }
        then show "nwdetect InterQ (ev_stm e)" by auto
      qed
      from a1 have d3:"nwdetect InterQ (ev_stm c)" using cs_regular by (metis csi.simps)
      from a0 c3 have "globev tr u \<and> globev tr c" by simp
      from c0 this d0 d1 d2 d3 show ?thesis using lem_ev_astmcl nwdetect_seqcond by metis
    qed
    moreover from c3 c0 have "wdetect InterQ (ev_stm u)" using lem_wdet by metis
    ultimately have "vdetect (ev_stm u) = Some T" using a0 a1 wint_value_Q
      by (auto simp add: qsrc_def wh_bdy_def waitstmQ_def)
    from c3 c0 this show ?thesis using lem_vdet by blast
  qed
  ultimately show ?thesis by blast
qed

lemma lem_lastwintQ: --"axiom"
  fixes tr c u
  assumes a0:"prog_semantics petalg tr \<and> globev tr c"
  assumes a1:"Qi c \<and> csi c \<and> w_interQi tr c = Some u"
  shows "\<forall>a. globev tr a \<and> Qi a \<and> a \<in> {u..c} \<and> writeto_ge InterQ a \<longrightarrow> a = u"
proof clarify
  fix e
  assume c0:"globev tr e" "Qi e" "e \<in> {u..c}" "writeto_ge InterQ e"
  obtain cond where c1:"cond = (\<lambda> e'. globev tr e' \<and> writeto_ge InterQ e' \<and> Qi e')" by blast
  from a1 c1 have "lastev cond c = Some u" by simp
  then have c2:"cond u \<and> (\<forall> a'. a' \<preceq> c \<and> cond a' \<longrightarrow> a' \<preceq> u)" using lem_lastev_some by blast
  from c0 c1 c2 have d1:"e \<preceq> u \<and> u \<preceq> e" by auto
  from c2 c1 c0 have d2:"globev tr e \<and> globev tr u" by auto
  from c2 c1 c0 have d3:"\<exists> p . is_proc_ev p u \<and> is_proc_ev p e" by auto
  from a0 d2 d3 have "e = u \<or> e \<prec> u \<or> u \<prec> e" using langevents.axlin by blast
  from this d1 show "e = u" by (metis less_le_not_le)
qed

lemma lem_wintPQ: --"axiom"
  fixes tr e
  assumes a0:"prog_semantics petalg tr \<and> globev tr e"
  assumes a1:"writeto_ge InterP e \<and> Qi e"
  shows "False"
proof -
  from a0 a1 have "stmcl (proc_stm qsrc) (ev_stm e)" using Qi_stmcl by metis
  moreover from a1 have "wdetect InterP (ev_stm e)" using lem_wdet a0 prog_semantics_def by metis
  moreover have "\<forall> s. stmcl (proc_stm qsrc) s \<and> wdetect InterP s \<longrightarrow> False"
    apply(auto)
    apply(case_tac s, simp_all)
    apply(case_tac "stmt1", auto)
    by (auto simp add: qsrc_def)
  ultimately show ?thesis by blast
qed

lemma lem_wturnQ_helper:
  fixes tr e
  assumes a0:"prog_semantics petalg tr \<and> globev tr e"
  assumes a1:"writeto_ge Turn e \<and> Qi e"
  shows "ge_val e = Some AP"
proof -
  from a0 a1 have "stmcl (proc_stm qsrc) (ev_stm e)" using Qi_stmcl by metis
  moreover from a1 have "wdetect Turn (ev_stm e)" using lem_wdet a0 prog_semantics_def by metis
  moreover have "\<And> s. stmcl (proc_stm qsrc) s \<and> wdetect Turn s \<longrightarrow> vdetect s = Some AP"
    apply(case_tac s)
    apply(auto simp add: qsrc_def)
    by (case_tac "stmt1", auto)
  ultimately have "vdetect (ev_stm e) = Some AP" by blast
  from this a0 show "ge_val e = Some AP" using lem_vdet prog_semantics_def by blast
qed

lemma lem_wturnQ: --"axiom"
  fixes tr c w
  assumes a0:"prog_semantics petalg tr \<and> globev tr c"
  assumes a1:"Qi c \<and> csi c \<and> w_turnQi tr c = Some u"
  shows "globev tr u \<and> writeto_ge Turn u \<and> ge_val u = Some AP"
proof -
  obtain cond where c1:"cond = (\<lambda> e'. globev tr e' \<and> writeto_ge Turn e' \<and> Qi e')" by blast
  from a1 c1 have "lastev cond c = Some u" by simp
  then have "cond u" using lem_lastev_some by blast
  from this c1 have c2:"globev tr u \<and> writeto_ge Turn u \<and> Qi u" by simp
  from a0 this have "ge_val u = Some AP" using lem_wturnQ_helper by blast
  from this c2 show ?thesis by blast
qed

lemma lem_lastwturQ: --"axiom"
  fixes tr c w
  assumes a0:"prog_semantics petalg tr \<and> globev tr c"
  assumes a1:"Qi c \<and> csi c \<and> w_turnQi tr c = Some w"
  shows "\<forall>a. globev tr a \<and> Qi a \<and> a \<in> {w..c} \<and> writeto_ge Turn a \<longrightarrow> a = w"
proof clarify
  fix e
  assume c0:"globev tr e" "Qi e" "e \<in> {w..c}" "writeto_ge Turn e"
  obtain cond where c1:"cond = (\<lambda> e'. globev tr e' \<and> writeto_ge Turn e' \<and> Qi e')" by blast
  from a1 c1 have "lastev cond c = Some w" by simp
  then have c2:"cond w \<and> (\<forall> a'. a' \<preceq> c \<and> cond a' \<longrightarrow> a' \<preceq> w)" using lem_lastev_some by blast
  from c0 c1 c2 have d1:"e \<preceq> w \<and> w \<preceq> e" by auto
  from c2 c1 c0 have d2:"globev tr e \<and> globev tr w" by auto
  from c2 c1 c0 have d3:"\<exists> p . is_proc_ev p w \<and> is_proc_ev p e" by auto
  from a0 d2 d3 have "e = w \<or> e \<prec> w \<or> w \<prec> e" using langevents.axlin by blast
  from this d1 show "e = w" by (metis less_le_not_le)
qed

lemma lem_wturnrQ: --"axiom"
  fixes tr e
  assumes a0:"prog_semantics petalg tr \<and> globev tr e"
  assumes a1:"writeto_ge Turn e \<and> ge_val e = Some AQ \<and> Qi e"
  shows "False"
using a0 a1
apply(subgoal_tac "ge_val e = Some AP")
apply(clarsimp)
apply(metis lem_wturnQ_helper)
done

lemma lem_srQ: --"axiom"
  fixes tr c r
  assumes a0:"prog_semantics petalg tr \<and> globev tr c"
  assumes a1:"Qi c \<and> csi c \<and> srQi tr c = Some r"
  shows "globev tr r \<and> (read_ge InterP r \<and> ge_val r = Some F \<or> read_ge Turn r \<and> ge_val r = Some AQ)"
proof -
  obtain cond where c1:"cond = (\<lambda> r . globev tr r \<and> stmlab (fseq (ev_stm r)) = None \<and> ((read_ge InterP r \<and> ge_val r = Some F) \<or> (read_ge Turn r \<and> ge_val r = Some AQ)) \<and> Qi r)" by blast
  from a1 c1 have "lastev cond c = Some r" by simp
  then have "cond r" using lem_lastev_some by blast
  from this c1 show ?thesis by blast
qed

lemma lem_cordQ: --"axiom"
  fixes tr
  and c::"((procnames, 'n, shnames, lbs) gevent)"
  assumes a0:"prog_semantics petalg tr \<and> globev tr c"
  assumes a1:"Qi c \<and> csi c"
  shows "\<exists> u w r. globev tr u \<and> globev tr w \<and> globev tr r \<and> Qi u \<and> Qi w \<and> Qi r \<and> w_interQi tr c = Some u \<and> w_turnQi tr c = Some w \<and> srQi tr c = Some r \<and> u \<prec> w \<and> w \<prec> r \<and> r \<prec> c"
proof -
  from a0 have c0:"valid_gtrace tr" using prog_semantics_def by blast
  obtain A_int where c1:"A_int = (\<lambda> e'. globev tr e' \<and> writeto_ge InterQ e' \<and> Qi e')" by blast
  obtain A_turn where c2:"A_turn = (\<lambda> e' . globev tr e' \<and> writeto_ge Turn e' \<and> Qi e')" by blast
  obtain A_sr where c3:"A_sr = (\<lambda> r . globev tr r \<and> stmlab (fseq (ev_stm r)) = None \<and> (read_ge InterP r \<and> ge_val r = Some F \<or> read_ge Turn r \<and> ge_val r = Some AQ) \<and> Qi r)" by blast

  have "\<exists> u1 . u1 \<preceq> c \<and> A_int u1"
  proof -
    { assume "\<forall> e' \<le> c . globev tr e' \<and> ge_proc e' = ProcQ \<longrightarrow> nwdetect InterQ (ev_stm e')"
      moreover from a1 have "ProcQ = proc_name qsrc \<and> ProcQ = ge_proc c" by (simp only: Qi.simps, normalization)
      moreover have "qsrc \<in> set petalg" by normalization
      ultimately have "astmcl (nwdetect InterQ) (proc_stm qsrc) (ev_stm c)" using a0 nwdetect_seqcond lem_init_astmcl by metis
      from this a1 have "False" using ex_wint_bef_cs_Q by (simp only: csi.simps, blast)
    }
    then obtain u1 where "u1 \<preceq> c \<and> globev tr u1 \<and> Qi u1 \<and> wdetect InterQ (ev_stm u1)" by (metis Qi.simps nwdetect.simps)
    moreover then have "writeto_ge InterQ u1" using c0 lem_wdet by metis
    ultimately show ?thesis using c1 by auto
  qed
  from this c1 obtain u where d1:"w_interQi tr c = Some u" using lem_lastev_val by auto
  from this c1 have d1':"A_int u \<and> u \<preceq> c" using lem_lastev_some by (auto simp only: w_interQi.simps)
  from this c1 have d1'':"globev tr u \<and> Qi u" by simp

  have "\<exists> w1 . w1 \<preceq> c \<and> A_turn w1"
  proof -
    { assume "\<forall> e' \<le> c . globev tr e' \<and> ge_proc e' = ProcQ \<longrightarrow> nwdetect Turn (ev_stm e')"
      moreover from a1 have "ProcQ = proc_name qsrc \<and> ProcQ = ge_proc c" by (simp only: Qi.simps, normalization)
      moreover have "qsrc \<in> set petalg" by normalization
      ultimately have "astmcl (nwdetect Turn) (proc_stm qsrc) (ev_stm c)" using a0 nwdetect_seqcond lem_init_astmcl by metis
      from this a1 have "False" using ex_wtur_bef_cs_Q by (simp only: csi.simps, blast)
    }
    then obtain u1 where "u1 \<preceq> c \<and> globev tr u1 \<and> Qi u1 \<and> wdetect Turn (ev_stm u1)" by (metis Qi.simps nwdetect.simps)
    moreover then have "writeto_ge Turn u1" using c0 lem_wdet by metis
    ultimately show ?thesis using c2 by auto
  qed
  from this c2 obtain w where d2:"w_turnQi tr c = Some w" using lem_lastev_val by auto
  from this c2 have d2':"A_turn w \<and> w \<preceq> c" using lem_lastev_some by (auto simp only: w_turnQi.simps)
  from this c2 have d2'':"globev tr w \<and> Qi w" by simp

  have er1: "\<exists> r1 . r1 \<preceq> c \<and> A_sr r1 \<and> w \<prec> r1"
  proof -
    {
      assume "astmcl (\<lambda> s. fseq s \<noteq> waitstmQ) (ev_stm w) (ev_stm c)"
      moreover from a0 d2'' have "stmcl (proc_stm qsrc) (ev_stm w)" using Qi_stmcl by blast
      moreover from a1 have "csdetect (ev_stm c)" by simp
      ultimately have "nwdetect Turn (ev_stm w)" using wait_bef_cs_Q by (auto simp add: qsrc_def wh_bdy_def waitstmQ_def)
      moreover from d2' c2 have "writeto_ge Turn w" by simp
      ultimately have "False" using c0 d2'' by (auto simp only: lem_wdet nwdetect.simps)
    }
    moreover from a0 d2' d2'' a1 have "w \<preceq> c \<and> ge_proc w = ProcQ \<and> ge_proc c = ProcQ" by simp
    moreover from a1 have "(\<lambda> s . fseq s \<noteq> waitstmQ) (ev_stm c)" by (simp add: waitstmQ_def)
    moreover have "seqcond (\<lambda> s. fseq s \<noteq> waitstmQ)" by (auto simp add: seqcond_def)
    ultimately obtain r1 where z1:"r1 \<in> {w<..c} \<and> globev tr r1 \<and> ge_proc r1 = ProcQ \<and> \<not> (\<lambda> s . fseq s \<noteq> waitstmQ) (ev_stm r1)" using c0 a0 d2'' lem_ev_astmcl [of "\<lambda> s . fseq s \<noteq> waitstmQ" tr w c ProcQ] by metis
    then have z2:"r1 \<preceq> c \<and> globev tr r1 \<and> Qi r1" by simp
    moreover have "read_ge InterP r1 \<and> ge_val r1 = Some F \<or> read_ge Turn r1 \<and> ge_val r1 = Some AQ"
    proof -
      from z1 have g0:"fseq (ev_stm r1) = waitstmQ" by simp
      then have "read_ge InterP r1 \<or> read_ge Turn r1" using waitstmQ_rdet c0 z2 lem_rdet by metis
      moreover have "read_ge InterP r1 \<longrightarrow> ge_val r1 = Some F"
      proof
        assume "read_ge InterP r1"
        moreover then obtain a where g1:"ge_val r1 = Some a" using read_ge_val by metis
        ultimately have h1:"\<And> wcs . wcsdetect (ev_stm r1) = Some wcs \<Longrightarrow> r_compat_wcs InterP a wcs" using lem_wcsdet [of tr r1 InterP a] using c0 z2 by blast
        moreover have "wcsdetect (ev_stm r1) = Some wcsQ"
        proof -
          have "\<And> s . fseq s = waitstmQ \<longrightarrow> wcsdetect s = Some wcsQ" by (induct_tac s, auto simp add: waitstmQ_def)
          from this g0 show ?thesis by blast
        qed
        ultimately have "r_compat_wcs InterP a (wcsQ::('n,shnames) wconds)" by metis
        then have "a = F" by (simp add: r_compat_wcs_def wcsQ_def)
        from this g1 show "ge_val r1 = Some F"  by simp
      qed
      moreover have "read_ge Turn r1 \<longrightarrow> ge_val r1 = Some AQ"
      proof
        assume "read_ge Turn r1"
        moreover then obtain a where g1:"ge_val r1 = Some a" using read_ge_val by metis
        ultimately have h1:"\<And> wcs . wcsdetect (ev_stm r1) = Some wcs \<Longrightarrow> r_compat_wcs Turn a wcs" using lem_wcsdet [of tr r1 Turn a] using c0 z2 by blast
        moreover have "wcsdetect (ev_stm r1) = Some wcsQ"
        proof -
          have "\<And> s . fseq s = waitstmQ \<longrightarrow> wcsdetect s = Some wcsQ" by (induct_tac s, auto simp add: waitstmQ_def)
          from this g0 show ?thesis by blast
        qed
        ultimately have "r_compat_wcs Turn a (wcsQ::('n,shnames) wconds)" by metis
        then have "a = AQ" by (simp add: r_compat_wcs_def wcsQ_def)
        from this g1 show "ge_val r1 = Some AQ"  by simp
      qed
      ultimately show ?thesis by blast
    qed
    moreover from z1 have "stmlab (fseq (ev_stm r1)) = None" by (simp add: waitstmQ_def)
    ultimately have "r1 \<preceq> c \<and> A_sr r1" using c3 by simp
    from this z1 show ?thesis by auto
  qed
  then have "\<exists> r1 . r1 \<preceq> c \<and> A_sr r1" by blast
  from this c3 obtain r where d3:"srQi tr c = Some r" using lem_lastev_val by auto
  from this c3 have d3':"A_sr r \<and> r \<preceq> c" using lem_lastev_some by (auto simp only: srQi.simps)
  from this c3 have d3'':"globev tr r \<and> Qi r" by simp

  have f0:"\<And> e1 e2 . Qi e1 \<and> globev tr e1 \<and> Qi e2 \<and> globev tr e2 \<and> (e2 \<preceq> e1 \<longrightarrow> False) \<longrightarrow> e1 \<prec> e2"
  proof
    fix e1 e2
    assume z0:"Qi e1 \<and> globev tr e1 \<and> Qi e2 \<and> globev tr e2 \<and> (e2 \<preceq> e1 \<longrightarrow> False)"
    then have "ge_proc e1 = ge_proc e2 \<and> globev tr e1 \<and> globev tr e2" by simp
    from this c0 have "e1 = e2 \<or> e1 \<prec> e2 \<or> e2 \<prec> e1" using lem_lin by blast
    from this z0 show "e1 \<prec> e2" by (metis order_less_imp_le order_refl)
  qed

  have f1:"w \<preceq> u \<longrightarrow> False"
  proof
    assume z1:"w \<preceq> u"
    from a0 d2'' have "stmcl (proc_stm qsrc) (ev_stm w)" using Qi_stmcl by blast
    moreover from c0 c2 d2' have "wdetect Turn (ev_stm w)" using lem_wdet by metis
    moreover from c0 d1'' d2'' z1 have "stmcl (ev_stm w) (ev_stm u)"
      by (subgoal_tac "ge_proc u = ProcQ \<and> ge_proc w = ProcQ", metis lem_ev_stmcl, auto)
    moreover have "astmcl (nwdetect Turn) (ev_stm u) (ev_stm c)"
    proof -
      have "\<forall> e \<in> {u<..c} . globev tr e \<and> ge_proc e = ProcQ \<longrightarrow> nwdetect Turn (ev_stm e)"
      proof clarify
        fix e
        assume y1:"e \<in> {u<..c}" "globev tr e" "ge_proc e = ProcQ"
        {
          assume "wdetect Turn (ev_stm e)"
          from this y1 c0 have "writeto_ge Turn e" using lem_wdet by metis
          from this c2 y1 have "e \<preceq> c \<and> A_turn e" by simp
          from this y1 d2 c2 have "e \<preceq> w" using lem_lastev_some [of "A_turn" c w] by auto
          moreover from y1 z1 have "w \<prec> e" by (auto simp add: order_le_less_trans)
          ultimately have "False" by (metis less_le_not_le)
        }
        then show "nwdetect Turn (ev_stm e)" by auto
      qed
      moreover from a1 have "nwdetect Turn (ev_stm c)" by (simp only: csi.simps cs_regular)
      moreover from d1'' a1 a0 have "ge_proc u = ProcQ \<and> ge_proc c = ProcQ" by simp
      ultimately show ?thesis using d1' d1'' a0 a1 c0 nwdetect_seqcond lem_ev_astmcl [of "nwdetect Turn" tr u c ProcQ] by metis
    qed
    moreover from a1 have "csdetect (ev_stm c)" by simp
    ultimately have "\<not> wdetect InterQ (ev_stm u)" using nowint_aft_tur_Q by (auto simp add: qsrc_def wh_bdy_def waitstmQ_def)
    from this c0 c1 d1' show "False" using lem_wdet by metis
  qed
  from this d1'' d2'' have or1:"u \<prec> w" using f0 by blast

  have or2:"r \<prec> c"
  proof-
    from d3'' a1 have "ge_proc r = ge_proc c" by simp
    from d3'' a1 a0 this have "r = c \<or> r \<prec> c \<or> c \<prec> r" using lem_lin c0 by blast
    moreover from a1 c3 d3' have "r \<noteq> c" by auto (* use labels Some lcs and None *)
    ultimately show ?thesis using d3' by (metis less_le_not_le)
  qed

  have or3:"w \<prec> r"
  proof -
    from er1 obtain r1 where z1:"r1 \<preceq> c \<and> A_sr r1 \<and> w \<prec> r1" by blast
    moreover have "r1 \<preceq> r"
    proof -
      from d3 c3 have "lastev A_sr c = Some r" by simp
      from this z1 show ?thesis using lem_lastev_some [of A_sr c r] by blast
    qed
    ultimately show ?thesis using or2 by (metis order_less_le_trans)
  qed

  from d1 d1'' d2 d2'' d3 d3'' or1 or2 or3 show ?thesis by blast
qed


(*------------------------------------------------------------------------------------------------------------------------------------------------------*)

interpretation petevent: Events_Peterson
  "prog_semantics" --"trace"
  "globev"         --"ev"
  "is_proc_ev"     --"proc"
  "read_ge"        --"read"
  "writeto_ge"     --"writeto"
  "ge_val"         --"val"
  "petalg"         --"ME"
  "Pi" "Qi" "csi"
  "w_interPi" "w_turnPi" "srPi"
  "w_interQi" "w_turnQi" "srQi"
apply(unfold_locales)
apply(metis lem_complpq)
apply(metis lem_linpq)
apply(metis lem_winterP)
apply(metis lem_lastwintP)
apply(metis lem_wintQP)
apply(metis lem_wturnP)
apply(metis lem_lastwturP)
apply(metis lem_wturnrP)
apply(metis lem_srP)
apply(metis lem_cordP)
apply(metis lem_winterQ)
apply(metis lem_lastwintQ)
apply(metis lem_wintPQ)
apply(metis lem_wturnQ)
apply(metis lem_lastwturQ)
apply(metis lem_wturnrQ)
apply(metis lem_srQ)
apply(metis lem_cordQ)
done

end
